Insert raw commands into .smt2 file with #![raw_command()] attribute by coeff-aij · Pull Request #21 · coord-e/thrust

coeff-aij · 2026-01-11T17:14:40Z

This attribute allows users to inject arbitrary string literals directly into the generated .smt2 files using crate-level inner attributes.

Usage
By adding an inner attribute to the crate root, such as:

#![feature(custom_inner_attributes)]
#![thrust::raw_command("(define-fun is_double ((x Int) (doubled_x Int)) Bool
    (=
        (* x 2)
        doubled_x
    )
)")]

// -- snip --

The attached string literal will be inserted into the head of the generated SMT-LIB2 file:

(set-logic HORN)

(define-fun is_double ((x Int) (doubled_x Int)) Bool
    (=
        (* x 2)
        doubled_x
    )
)

; -- snip --

Motivation
This feature is intended for debugging and testing. It enables the manual injection of SMT-LIB logic, serving as a workaround until a dedicated parser is implemented.

coeff-aij · 2026-01-11T17:30:05Z

Probably I have to add some more tests and documentation comments.

coeff-aij · 2026-01-12T05:56:58Z

@@ -0,0 +1,20 @@
+//@error-in-other-file: UnexpectedToken


How can I test that the Thrust panics with a specific error message? I tried using //@error-in-other-file, but I might be misunderstanding its purpose.

I think testing panic messages is not possible with the current testing framework (ui_test https://docs.rs/ui_test/). However, I don't think we want tests for panicking cases anyway; it would be beneficial if we supported reporting rustc diagnostics for parse errors, but it's out of scope for now.

I've added the description about this situation as comments for now:

// This test panics with "invalid attribute" for now. // TODO: reporting rustc diagnostics for parse errors

coeff-aij · 2026-01-12T06:02:13Z

+            let ts = analyze::annot::extract_annot_tokens(attrs.clone());
+            let parser = annot::AnnotParser::new(
+                // TODO: this resolver is not actually used.
+                analyze::annot::ParamResolver::default()


parseg_raw_definition() is implemented on annot::AnnotParser and it's new() requires any Resolver instance, which isn't actually used in parsing of raw definitions.
I might have to fix so that no Resolver is required for this analysis.

I don't think it needs to be implemented in AnnotParser. How about extracting the string from the annotation in a method within crate_::Analyzer?

coord-e · 2026-01-13T14:23:10Z

+            let ts = analyze::annot::extract_annot_tokens(attrs.clone());
+            let parser = annot::AnnotParser::new(
+                // TODO: this resolver is not actually used.
+                analyze::annot::ParamResolver::default()


I don't think it needs to be implemented in AnnotParser. How about extracting the string from the annotation in a method within crate_::Analyzer?

coord-e · 2026-01-13T14:36:05Z

@@ -0,0 +1,20 @@
+//@error-in-other-file: UnexpectedToken


I think testing panic messages is not possible with the current testing framework (ui_test https://docs.rs/ui_test/). However, I don't think we want tests for panicking cases anyway; it would be beneficial if we supported reporting rustc diagnostics for parse errors, but it's out of scope for now.

coord-e · 2026-01-13T14:37:15Z

+//@check-pass
+//@compile-flags: -Adead_code -C debug-assertions=off
+
+// Insert definitions written in SMT-LIB2 format into .smt file directly.


nit

Suggested change

// Insert definitions written in SMT-LIB2 format into .smt file directly.

// Insert definitions written in SMT-LIB2 format into .smt2 file directly.

To avoid using the AnnotParser and Parser, we need to move parse_annot_raw_definition() out of annot::Parser. However, doing so means it will lose access to the various parsing utilities and error definitions defined there.

Do you have any suggestions on how to handle this?

(maybe this #21 (comment))

Do you have any suggestions on how to handle this?

parse_annot_raw_definition just extracts a string literal from the TokenStream and not much else (so I'd rather call it "extract" than "parse"), so I think you can simply write that extraction directly in crate_::Analyzer without using utilities from AnnotParser. For errors, you can just panic! for now. I haven't tested it, but I think code like the following should work.

let raw_command = ts.iter().find_map(|tt| match tt { TokenTree::Token(Token { kind: TokenKind::Literal(lit), .. }, _) if lit.kind == LitKind::Str => Some(lit.symbol.to_string()), _ => None, }).expect("invalid raw_command annotation");

coord-e · 2026-01-13T14:38:03Z

+
+#[thrust::requires(true)]
+#[thrust::ensures(result == 2 * x)]
+// #[thrust::ensures(is_double(x, result))]


If you plan to uncomment this in a future PR, please add a note about it in the comments.

I forgot to delete them, but I have deleted them now.

coord-e · 2026-01-14T17:06:50Z

-        for (p, def) in self.inner.pred_vars.iter_enumerated() {
-            if !def.debug_info.is_empty() {
-                writeln!(f, "{}", def.debug_info.display("; "))?;
+        for (p, cmd) in self.inner.pred_vars.iter_enumerated() {
+            if !cmd.debug_info.is_empty() {
+                writeln!(f, "{}", cmd.debug_info.display("; "))?;
            }
            writeln!(
                f,
                "(declare-fun {} {} Bool)\n",
                p,
-                List::closed(def.sig.iter().map(|s| self.ctx.fmt_sort(s)))
+                List::closed(cmd.sig.iter().map(|s| self.ctx.fmt_sort(s)))


This seems to be an unrelated change.

…s TokenTrees directly

coord-e

LGTM. Thanks!

Co-authored-by: Hiromi Ogawa <me@coord-e.com>

coeff-aij commented Jan 12, 2026

View reviewed changes

This was referenced Jan 12, 2026

(WIP)Support annotations for predicates #20

Closed

Support user-defined predicate call in annotation #22

Merged

coord-e self-requested a review January 13, 2026 14:13

coord-e reviewed Jan 13, 2026

View reviewed changes

coeff-aij changed the title ~~Insert raw definition into .smt2 file with #![raw_definie()] attribute~~ Insert raw commands into .smt2 file with #![raw_command()] attribute Jan 14, 2026

coord-e reviewed Jan 14, 2026

View reviewed changes

coeff-aij force-pushed the raw-define branch 2 times, most recently from 55993e8 to 1434597 Compare January 18, 2026 15:16

coord-e and others added 19 commits January 19, 2026 15:59

Run CI workflow on pull_request

7f68acf

add: test for raw_define attribute

9a0ee9b

add: RawDefinition for System

984c159

add: formatting for RawDefinition

209dfed

add: raw_define path

8c2716f

add: parse raw definitions

e19c5bc

fix: invalid SMT-LIB2 format

aab6bdc

add: analyze inner-attribute #[raw_define()] for the given crate

79813f2

fix: error relate to new raw_definitions field of System

f18c14d

remove: unused code

1b6658a

add: positiive test for multiple raw_define annotations

bdf5b4d

add: negative tests for raw_define

393e7e6

fix: tests for raw_define(removing unused code, add more description)

55bc858

change: rename raw_define -> raw_command, RawDefine -> RawCommand, etc.

5f8e80e

add: negative tests for raw_define

d9e4a93

remove: FormatContext::raw_commands

51f1afd

fix: wrong description about the error on negative test

c1458e6

fix: undo accidental renames

ace4d2a

change: delete annot::AnnotParser::parse_raw_definition() and procces…

bc79866

…s TokenTrees directly

fix: run cargo fmt

4937071

coeff-aij force-pushed the raw-define branch from 6061ee8 to 8273742 Compare January 19, 2026 07:05

remove: accidentally duplicated negative tests

49f5691

coeff-aij force-pushed the raw-define branch from 8273742 to 49f5691 Compare January 19, 2026 07:45

coord-e approved these changes Jan 20, 2026

View reviewed changes

Comment thread src/analyze/crate_.rs Outdated

Comment thread src/chc.rs Outdated

coeff-aij and others added 2 commits January 20, 2026 20:24

Update src/analyze/crate_.rs

cac76db

Co-authored-by: Hiromi Ogawa <me@coord-e.com>

Update src/chc.rs

f354b5d

Co-authored-by: Hiromi Ogawa <me@coord-e.com>

coeff-aij merged commit cd26f00 into coord-e:main Jan 20, 2026
3 checks passed

	// Insert definitions written in SMT-LIB2 format into .smt file directly.
	// Insert definitions written in SMT-LIB2 format into .smt2 file directly.

Conversation

coeff-aij commented Jan 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

coeff-aij commented Jan 11, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

coord-e left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

coeff-aij commented Jan 11, 2026 •

edited

Loading